Nuprl Lemma : decidable__atom_equal_2
11,40
postcript
pdf
a
,
b
:atom{2:n}. decidable((
a
=
b
))
latex
Definitions
False
,
P
Q
,
A
,
prop{i:l}
,
P
Q
,
t
T
,
decidable(
P
)
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
origin
a,b:atom{2:n}. decidable((a = b)) a,b:atom{2:n}. decidable((a = b)) 
Q
A
Q
Tx:A. B(x)